Hi,

I have re-run a new version of the model, which discovered 7 additional proofs: 5740c4a

Thank you for sharing the proofs! I'm not sure whether we should continue to add proofs to minif2f though because it will lead to training data contamination with Github being a classical source of pretraining data. I will leave it open for now :)

I totally understand. Feel free to close this PR as you see appropriate.

Let's leave it open for visibility :)

@yangky11 What model did you use?

Hi @yangky11 , I have the same question as @Adarsh321123

I think this is the LeanDojo / ReProver paper: https://arxiv.org/abs/2306.15626

I think this is the LeanDojo / ReProver paper: https://arxiv.org/abs/2306.15626

Yes, but we no longer maintain the Lean 3 model since people have switched to Lean 4.